/*!
 * \file set_relation_isl_visitor_test.cc
 *
 * \brief Set and Relation isl visitor tests
 *
 * This file is to test the isl visitor of the set and relation classes. The
 * isl visitor should be able to take in any sort of valid input and then
 * create a string that is equivelent to the original string.
 *
 * \date Started: 6/8/2010
 * \date Last Modified: 7/27/2010
 * \authors Alan LaMielle
 * \authors Ian Craig
 * \authors Nicholas Jeanette
 *
 * Copyright (c) 2010, Colorado State University <br>
 * All rights reserved. <br>
 * See ../../COPYING for details. <br>
 */

#include <iegenlib/iegenlib.h>

#include <gtest/gtest.h>
#include <iostream>

using iegenlib::IEGenLibContext;
using iegenlib::Set;
using iegenlib::Relation;
using iegenlib::Symbolic;

//NOTE SHOULD TEST WITH SYMBOLICS

TEST(SetISL, simple1) {
   Set s("{[]}");
   EXPECT_EQ(s.get_isl(),"{[]}");
}

TEST(SetISL, simple2) {
   Set s("{[x]}");
   EXPECT_EQ(s.get_isl(),"{[x]}");
}

TEST(SetISL, simple3) {
   Set s("{[x,y]}");
   EXPECT_EQ(s.get_isl(),"{[x,y]}");
}

TEST(SetISL, simple4) {
   Set s("{[1,x]}");
   EXPECT_EQ(s.get_isl(),"{[1,x]}");
}

TEST(SetISL, simple5) {
   Set s("{[x,1]}");
   EXPECT_EQ(s.get_isl(),"{[x,1]}");
}

TEST(SetISL, simple6) {
   Set s("{[x,y] : x >= 1 and y < x }");
   EXPECT_EQ(s.get_isl(),"{[x,y] : x-y-1>=0 and x-1>=0}");
}

TEST(SetISL, simple7) {
   Set s("{[x,y] : x < z}");
   Set expected("{[x,y] : exists(z : -x+z-1>=0)}");
   EXPECT_EQ(s, expected);
   EXPECT_EQ(s.get_isl(),"{[x,y]}");
}

TEST(SetISL, simple8) {
   Set s("{[x,y]: x = y}");
   EXPECT_EQ(s.get_isl(),"{[x,y] : x-y=0}");
}

TEST(SetISL, simple9) {
   Set s("{[x,y,z]: x = z and y = z}");
   Set expected("{[x,y,z] : y-z=0 and x-z=0}");
   EXPECT_EQ(s, expected);
   EXPECT_EQ(s.get_isl(),"{[x,y,z] : x-y=0 and x-z=0}");
}


TEST(SetISL, simple10) {
   Set s("{[1,x]: x > 1}");
   EXPECT_EQ(s.get_isl(),"{[1,x] : x-2>=0}");
}

TEST(SetISL, dups1) {
   Set s ("{[x,x]}");
   EXPECT_EQ(s.get_isl(),"{[x,x1] : x-x1=0}");
}

TEST(SetISL, dups2) {
   Set s("{[x,y,x]}");
   EXPECT_EQ(s.get_isl(),"{[x,y,x1] : x-x1=0}");
}

TEST(SetISL, dups3) {
   Set s("{[x,y,x] : x<y+3}");
   EXPECT_EQ(s.get_isl(),"{[x,y,x1] : x-x1=0 and -x+y+2>=0}");
}

TEST(SetISL, dups4) {
   Set s("{[x,y,x] : x = y}");
   EXPECT_EQ(s.get_isl(),"{[x,y,x1] : x-x1=0 and x-y=0}");
}

TEST(SetISL, dups5) {
   Set s("{[x,x,x]}");
   EXPECT_EQ(s.get_isl(),"{[x,x1,x2] : x-x1=0 and x-x2=0}");
}

TEST(SetISL, function0) {
   Set s("{[x] : f(x)>0}");
   EXPECT_EQ(s.get_isl(),"{[x] : f(x)-1>=0}");
}

TEST(SetISL, function1) {
   Set s("{[x,y] : f(x,y)=0}");
   EXPECT_EQ(s.get_isl(),"{[x,y] : f(x,y)=0}");
}

TEST(SetISL, function2) {
   Set s("{[x,x] : f(x,x)=0}");
   EXPECT_EQ(s.get_isl(),"{[x,x1] : f(x,x)=0 and x-x1=0}");
}

TEST(SetISL, function3) {
   Set s("{[x,x] : f(x,g(x))=0}");
   EXPECT_EQ(s.get_isl(),"{[x,x1] : f(x,g(x))=0 and x-x1=0}");
}

TEST(SetISL, function4) {
   Set s("{[x,y] : f(x,1)=0}");
   EXPECT_EQ(s.get_isl(),"{[x,y] : f(x,1)=0}");
}

TEST(SetISL, function5) {
   Set s("{[x,2] : f(x,y)=0}");
   EXPECT_EQ(s.get_isl(),"{[x,2] : exists(y : f(x,y)=0)}");
}

TEST(SetISL, function6) {
   Set s("{[x] : f(1)>0}");
   EXPECT_EQ(s.get_isl(),"{[x] : f(1)-1>=0}");
}

TEST(SetISL, function7) {
   Set s("{[x,y] : y=f(x,g(y))}");
   EXPECT_EQ(s.get_isl(),"{[x,y] : y-f(x,g(y))=0}");
}

TEST(SetISL, functionDuplicateFunctionEqualities) {
   Set s("{[x,2] : f(x,y)=0 and f(x,y)=0}");
   EXPECT_EQ(s.get_isl(),"{[x,2] : exists(y : f(x,y)=0)}");
}

TEST(SetISL, functionInFuntion) {
   Set s("{[x,y] : y = f(x,g(y))}");
   EXPECT_EQ(s.get_isl(),"{[x,y] : y-f(x,g(y))=0}");
}

TEST(SetISL, exists1) {
   IEGenLibContext context;
   context.setSimplifyConjunctions(false);
   Set s("{[x,y] : y = e}",context);
   EXPECT_EQ(s.get_isl(),"{[x,y] : exists(e : y-e=0)}");
}

TEST(SetISL, exists2) {
   IEGenLibContext context;
   context.setSimplifyConjunctions(false);
   Set s("{[x,y] : y = e and x=f}",context);
   EXPECT_EQ(s.get_isl(),"{[x,y] : exists(e,f : y-e=0 and x-f=0)}");
}

TEST(SetISL, exists3) {
   IEGenLibContext context;
   context.setSimplifyConjunctions(false);
   Set s("{[x,y] : y = e and x=f and g=10}",context);
   EXPECT_EQ(s.get_isl(),"{[x,y] : exists(e,f,g : g-10=0 and y-e=0 and x-f=0)}");
}

TEST(RelationISL, simpleRel1) {
   Relation r("{[]->[]}");
   EXPECT_EQ(r.get_isl(),"{[]->[]}");
}

TEST(RelationISL, simpleEmptyIn) {
   Relation r("{[]->[a,b]}");
   EXPECT_EQ(r.get_isl(),"{[]->[a,b]}");
}

//Test for bug #416
TEST(RelationISL, simpleEmptyOut) {
   Relation r("{[a,b]->[]}");
   EXPECT_EQ(r.get_isl(),"{[a,b]->[]}");
}

TEST(RelationISL, simpleRel2) {
   Relation r("{[x]->[x]}");
   EXPECT_EQ(r.get_isl(),"{[x]->[x1] : x-x1=0}");
}

TEST(RelationISL, simpleRel3) {
   Relation r("{[x,y]->[x]}");
   EXPECT_EQ(r.get_isl(),"{[x,y]->[x1] : x-x1=0}");
}

TEST(RelationISL, simpleRel4) {
   Relation r("{[1,x]->[x,1]}");
   EXPECT_EQ(r.get_isl(),"{[1,x]->[x1,1] : x-x1=0}");
}

TEST(RelationISL, simpleRel5) {
   Relation r("{[x,1]->[w,y,z]}");
   EXPECT_EQ(r.get_isl(),"{[x,1]->[w,y,z]}");
}

TEST(RelationISL, simpleRel6) {
   Relation r("{[x,y]->[x,y] : x >= 1 and y < x }");
   EXPECT_EQ(r.get_isl(),"{[x,y]->[x1,y1] : y-y1=0 and x-x1=0 and x-y-1>=0 and x-1>=0}");
}

TEST(RelationISL, simpleRel7) {
   Relation r("{[x,y]->[x,y] : x < z}");
   Relation expected("{[x,y]->[x1,y1] : exists(z : y-y1=0 and x-x1=0 and -x+z-1>=0)}");
   EXPECT_EQ(r, expected);
   EXPECT_EQ(r.get_isl(),"{[x,y]->[x1,y1] : y-y1=0 and x-x1=0}");
}

TEST(RelationISL, simpleRel8) {
   Relation r("{[x,y]->[x,y]: x = y}");
   Relation expected("{[x,y]->[x1,y1] : y-y1=0 and x-x1=0 and x-y=0}");
   EXPECT_EQ(r, expected);
   EXPECT_EQ(r.get_isl(),"{[x,y]->[x1,y1] : x-x1=0 and x-y=0 and x-y1=0}");
}

TEST(RelationISL, dupsRel1) {
   Relation r("{[x,x]->[x,x]}");
   EXPECT_EQ(r.get_isl(),"{[x,x1]->[x2,x3] : x-x1=0 and x-x2=0 and x-x3=0}");
}

TEST(RelationISL, dupsRel2) {
   Relation r("{[x,y,x]->[x,y,x]}");
   EXPECT_EQ(r.get_isl(),"{[x,y,x1]->[x2,y1,x3] : y-y1=0 and x-x1=0 and x-x2=0 and x-x3=0}");
}

TEST(RelationISL, dupsRel3) {
   Relation r("{[x,y,x]->[x,y,x] : x<y+3}");
   EXPECT_EQ(r.get_isl(),"{[x,y,x1]->[x2,y1,x3] : y-y1=0 and x-x1=0 and x-x2=0 and x-x3=0 and -x+y+2>=0}");
}

TEST(RelationISL, functionRel0) {
   Relation r("{[x]->[x] : f(x)>0}");
   EXPECT_EQ(r.get_isl(),"{[x]->[x1] : x-x1=0 and f(x)-1>=0}");
}

TEST(RelationISL, functionRel1) {
   Relation r("{[x,y]->[x,y] : f(x,y)=0}");
   EXPECT_EQ(r.get_isl(),"{[x,y]->[x1,y1] : f(x,y)=0 and y-y1=0 and x-x1=0}");
}

TEST(RelationISL, functionRel2) {
   Relation r("{[x,x]->[y,y] : f(x,x)=0}");
   EXPECT_EQ(r.get_isl(),"{[x,x1]->[y,y1] : f(x,x)=0 and y-y1=0 and x-x1=0}");
}

TEST(RelationISL, functionRel3) {
   Relation r("{[x,y]->[x,y] : f(x,1)=0}");
   EXPECT_EQ(r.get_isl(),"{[x,y]->[x1,y1] : f(x,1)=0 and y-y1=0 and x-x1=0}");
}

TEST(RelationISL, AlanRelation) {
   Relation r("{[a]->[b]:3f(5*g(2a,-5*a)-5)>=0}");
   EXPECT_EQ(r.get_isl(),"{[a]->[b] : 3f(5g(2a,-5a)-5)>=0}");
}

TEST(RelationISL, AlanRelation1) {
   Relation r("{[ii] -> [inter_func]: ii>=f(x)}");
   EXPECT_EQ(r.get_isl(),"{[ii]->[inter_func] : exists(x : ii-f(x)>=0)}");
}

TEST(RelationISL, AlanRelation2) {
   Relation r("{[a]->[b]:f(g(a,a))>=0}");
   EXPECT_EQ(r.get_isl(),"{[a]->[b] : f(g(a,a))>=0}");
}

TEST(RelationISL, AlanRelation3) {
   Relation r("{[4]->[5]}");
   EXPECT_EQ(r.get_isl(),"{[4]->[5]}");
}

TEST(RelationISL, UnionRelation) {
   Relation r("{[c]->[d]: d>=1 and c>2} union{[a]->[b]: a>=2 and b-1>0}");
   EXPECT_EQ(r.get_isl(),"{[c]->[d] : c-3>=0 and d-1>=0; [c]->[d] : d-2>=0 and c-2>=0}");
}

TEST(RelationISL, BlankRelation) {
   Relation r("{[]->[]}");
   EXPECT_EQ(r.get_isl(),"{[]->[]}");
}

TEST(RelationISL, Symbolics1) {
   IEGenLibContext context;
   context.addSymbolic(Symbolic("z"));
   Set s("{[x,y]: x = z and y = z}",context);
   EXPECT_EQ(s.get_isl(),"[z]->{[x,y] : z-x=0 and z-y=0}");
}

TEST(RelationISL, Symbolics2) {
   IEGenLibContext context;
   Set s("[z]->{[x,y]: x = z and y = z}",context);
   EXPECT_EQ(s.get_isl(),"[z]->{[x,y] : z-x=0 and z-y=0}");
}

TEST(RelationISL, exists1) {
   IEGenLibContext context;
   context.setSimplifyConjunctions(false);
   Relation r("{[x]->[y] : y = e}",context);
   EXPECT_EQ(r.get_isl(),"{[x]->[y] : exists(e : y-e=0)}");
}

TEST(RelationISL, exists2) {
   IEGenLibContext context;
   context.setSimplifyConjunctions(false);
   Relation r("{[x]->[y] : y = e and x=f}",context);
   EXPECT_EQ(r.get_isl(),"{[x]->[y] : exists(e,f : y-e=0 and x-f=0)}");
}

TEST(RelationISL, exists3) {
   IEGenLibContext context;
   context.setSimplifyConjunctions(false);
   Relation r("{[x]->[y] : y = e and x=f and g=10}",context);
   EXPECT_EQ(r.get_isl(),"{[x]->[y] : exists(e,f,g : g-10=0 and y-e=0 and x-f=0)}");
}
